\begin{tabbing}
$\forall$$A$:Type, $f$:($A$$\rightarrow\mathbb{B}$), $L$:$A$ List.
\\[0ex]$\forall$$a$$\in$$L$.
\\[0ex]($\forall$$b$$\geq$$a$$\in$$L$.$f$($b$))
\\[0ex]$\Rightarrow$ (\=$\exists$$L_{1}$, $L_{2}$:$A$ List.\+
\\[0ex]$L$ $=$ ($L_{1}$ @ $L_{2}$) $\in$ $A$ List \& ($a$ $\in$ $L_{2}$) \& ($\forall$$b$$\in$$L_{2}$. $f$($b$)) \& ($\neg$null($L_{1}$) $\Rightarrow$ $\neg$$f$(last($L_{1}$))))
\-
\end{tabbing}